👍 It's a rather delicate PR to merge, since other PR may be in conflict afther that (even if the merge system should work for basic stuff)

For me this is something that should be rapidly merged to avoid future other conflicts

git is usually quite good at figuring out moved files, as long as they do not change massively at the same time. lets see :-)